Nuprl Definition : es-first-at-since' 11,40
es-first-at-since'(es;i;e;e.R(e);e.P(e))
== loc(e) = i
== & R(e)
== & (e':E. ((e' <loc e) c (P(e') & (e'':E. e' loc e''   (e'' <loc e)  (R(e'')))))) 
latex

clarification:

es-first-at-since'(es;i;e;e.R(e);e.P(e))
== es-loc(es; e) = i  Id
== & R(e)
== & (e':es-E(es)
== & ((es-locl(es; e'; e)
== & (c (P(e') & (e'':es-E(es). es-le(es;e';e'')  es-locl(es; e''; e)  (R(e'')))))) 
latex

Definitionses-first-at-since'(es;i;e;e.R(e);e.P(e)), Id, loc(e), x:A. B(x), A c B, P & Q, x:A. B(x), E, e loc e' , P  Q, (e <loc e'), A
FDL editor aliaseses-first-at-since'

origin